ds:top, da:fpf(Knd; k.Type), x,T:top, ks:(Knd List), tr:top, j,i:Id.
R-da(R-state-var(i; ds; da; x; T; ks; tr); j)
=
if eq_id(i; j)
then reduce((k,d1. fpf-join(Kind-deq; fpf-single(k; ma-valtype(da; k)); d1)); fpf-empty; ks)
else fpf-empty
fi 
 fpf(Knd; k.Type) 

latex

Definitions	Y, reduce(f; k; as), ff, tt, if b then t else f fi , P  Q, P  Q, P  Q, P  Q, prop{i:l}, x. t(x), subtype(S; T), t  T, R-state-var(i; ds; da; x; T; ks; tr), R-da(R; i), top, x:A. B(x), Unit, , x(s),
Lemmas	not functionality wrt iff, assert of bnot, eqff to assert, assert-eq-id, eqtt to assert, iff transitivity, not wf, bnot wf, Kind-deq wf, ma-valtype wf, fpf-single wf3, fpf-join wf, reduce wf, fpf-empty-join, fpf-empty wf, assert wf, bool wf, eq id wf, fpf wf, Knd wf, top wf, Id wf, R-da-Rall